Nuprl Lemma : d-I_wf
0,22
postcript
pdf
i
:Id. Inlnk(
i
)
IdLnk
Prop
latex
Definitions
Inlnk(
i
)
,
Prop
,
destination(
l
)
,
x
:
A
.
B
(
x
)
,
IdLnk
,
t
T
,
Id
Lemmas
Id
wf
,
IdLnk
wf
,
ldst
wf
origin
i:Id. Inlnk(i) 
IdLnk
Prop i:Id. Inlnk(i) IdLnkProp x:A. B(x) T